A, B:Type, L:((A(B + Top)) List), x:A.
(f,gL.  p-disjoint(A;f;g))
 (f:(A(B + Top)).
 (f  L)  (can-apply(f;x))  (do-apply(p-first(L);x) = do-apply(f;x)  B)) 

latex

Definitions

s = t, P  Q, x:A. B(x), do-apply(f;x), b, x:AB(x), P  Q, x:A  B(x), P & Q, P  Q, Top, left + right, (x  l), p-disjoint(A;f;g), (x,yL.  P(x;y)), type List, Type, Void, t  T, x:A.B(x), S  T, suptype(S; T), can-apply(f;x), , x:A. B(x), (xL.P(x)), x.A(x), filter(P;l), hd(l), False, A, A  B, i  j < k, , {x:A| B(x)} , {i..j}, [], l[i], a < b, [car / cdr], x,y. t(x;y), b, , Unit, A c B, , P  Q, Dec(P), #$n, i <z j, i z j, {T}, SQType(T), ||as||, s ~ t

Lemmas

cons member, pairwise-cons, length wf1, le wf, decidable int equal, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, pairwise wf, p-disjoint wf, nil member, int seg wf, can-apply-p-first, l member wf, assert wf, can-apply wf, top wf, do-apply-p-first, do-apply wf